$\forall$$T$:Type, ${\it ll}$:($T$ List) List, $x$:$T$. ($x$ $\in$ concat(${\it ll}$)) $\Leftrightarrow$ ($\exists$$l$:$T$ List. ($l$ $\in$ ${\it ll}$) \& ($x$ $\in$ $l$))